package auction;

import java.io.*;
import java.net.*;
import java.util.*;
import java.util.concurrent.*;

public class Program {
    public static void main(String[] args) throws IOException /*@ ensures true; @*/
        //@ requires true;
        //@ ensures true;
    {
        AuctionRoom auctionroom = new AuctionRoom();
        //@ close auctionroom_ctor(auctionroom)();
        //@ close n_times(0, auctionroom_ctor(auctionroom));
        //@ close n_times(1, auctionroom_ctor(auctionroom));
        Semaphore auctionroomLock = new Semaphore(1);
        ServerSocket serverSocket = new ServerSocket(12345);

        while (true)
            //@ invariant semaphore(?f, auctionroomLock, ?p, auctionroom_ctor(auctionroom)) &*& ServerSocket(serverSocket);
        {
            Socket socket = serverSocket.accept();
            //@ semaphore_split(auctionroomLock); 
            BidderSession biddersession = new BidderSession(auctionroom, auctionroomLock, socket);
            //@ close thread_run_pre(BidderSession.class)(biddersession, unit);
            Thread t = new Thread(biddersession);
            t.start();
        }
    }
}